M1 || M2
== M1 ||decl M2
== & (M1.2.2).1 || (M2.2.2).1
== & (M1.2.2.2).1 || (M2.2.2.2).1
== & (M1.2.2.2.2).1 || (M2.2.2.2.2).1
== & (M1.2.2.2.2.2).1 || (M2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2.2.2.2.2).1
== & (M1.2.2.2.2.2.2.2.2.2.2.2).1 || (M2.2.2.2.2.2.2.2.2.2.2.2).1 

latex

---

clarification:

ma-compatible{i:l}
ma-compatible(M1; M2)
== ma-compatible-decls{i:l}
== ma-compatible-decls(M1; M2)
== & fpf-compatible(Id;
== & fpf-compatible(x.(fpf-cap(fpf-join(IdDeq;M1.1;M2.1);IdDeq;x;Void));
== & fpf-compatible(IdDeq;
== & fpf-compatible(((M1.2.2).1);
== & fpf-compatible(((M2.2.2).1))
== & fpf-compatible(Id;
== & fpf-compatible(a.(State(fpf-join(IdDeq;M1.1;M2.1)));
== & fpf-compatible(IdDeq;
== & fpf-compatible(((M1.2.2.2).1);
== & fpf-compatible(((M2.2.2.2).1))
== & fpf-compatible((:Knd  Id);
== & fpf-compatible(kx.(State(fpf-join(IdDeq;M1.1;M2.1))
== & fpf-compatible(Valtype(fpf-join(KindDeq;(M1.2).1;(M2.2).1);kx.1)
== & fpf-compatible(fpf-cap(fpf-join(IdDeq;M1.1;M2.1);IdDeq;kx.2;Void));
== & fpf-compatible(product-deq(Knd;Id;KindDeq;IdDeq);
== & fpf-compatible(((M1.2.2.2.2).1);
== & fpf-compatible(((M2.2.2.2.2).1))
== & fpf-compatible
== ((:Knd  IdLnk);
== (kl.((tg:Id
== ( (State(fpf-join(IdDeq;M1.1;M2.1))Valtype(fpf-join(KindDeq;(M1.2).1;(M2.2).1);kl.1)
== ( (fpf-cap(fpf-join(KindDeq;(M1.2).1;(M2.2).1);KindDeq;rcv(kl.2,tg);Void) List))) List);
== (product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);
== (((M1.2.2.2.2.2).1);
== (((M2.2.2.2.2.2).1))
== & fpf-compatible(Id; x.(Knd List); IdDeq; ((M1.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2).1))
== & fpf-compatible((:IdLnk  Id);
== & fpf-compatible(lt.(Knd List);
== & fpf-compatible(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);
== & fpf-compatible(((M1.2.2.2.2.2.2.2).1);
== & fpf-compatible(((M2.2.2.2.2.2.2.2).1))
== & fpf-compatible(Knd; k.(Id List); KindDeq; ((M1.2.2.2.2.2.2.2.2).1); ((M2.2.2.2.2.2.2.2.2).1))
== & fpf-compatible(Knd;
== & fpf-compatible(k.(IdLnk List);
== & fpf-compatible(KindDeq;
== & fpf-compatible(((M1.2.2.2.2.2.2.2.2.2).1);
== & fpf-compatible(((M2.2.2.2.2.2.2.2.2.2).1))
== & fpf-compatible(Id;
== & fpf-compatible(x.(Knd List);
== & fpf-compatible(IdDeq;
== & fpf-compatible(((M1.2.2.2.2.2.2.2.2.2.2).1);
== & fpf-compatible(((M2.2.2.2.2.2.2.2.2.2.2).1))
== & fpf-compatible(Id;
== & fpf-compatible(x.FinProbSpace;
== & fpf-compatible(IdDeq;
== & fpf-compatible(((M1.2.2.2.2.2.2.2.2.2.2.2).1);
== & fpf-compatible(((M2.2.2.2.2.2.2.2.2.2.2.2).1)) 

latex

Definitions	M1 ||decl M2, , , State(ds), x:AB(x), Valtype(da;k), f(x)?z, f  g, rcv(l,tg), Void, x:A  B(x), product-deq(A;B;a;b), IdLnkDeq, IdLnk, KindDeq, P & Q, type List, Knd, f || g, Id, FinProbSpace, IdDeq, t.1, t.2
FDL editor aliases	ma-compatible